Conversation
fabiomadge
force-pushed
the
fabiomadge/constrained-types
branch
from
1c60132 to
b2d41d6
Compare
fabiomadge
force-pushed
the
fabiomadge/early-return-soundness
branch
3 times, most recently
from
579e349 to
dd1139d
Compare
fabiomadge
force-pushed
the
fabiomadge/constrained-types
branch
8 times, most recently
from
fa3f500 to
566122e
Compare
fabiomadge
changed the title
fabiomadge
force-pushed
the
fabiomadge/constrained-types
branch
from
566122e to
e2ff8b6
Compare
fabiomadge
force-pushed
the
fabiomadge/constrained-types
branch
5 times, most recently
from
9c8f422 to
afd9ee8
Compare
keyboardDrummer
left a comment
keyboardDrummer
left a comment
There was a problem hiding this comment.
Code quality looks great but I have some feedback on the design.
Also, could you add a test that compares the Laurel before and after the phase? Similar to StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
| assert y >= 0; | ||
| } | ||
|
|
||
| // Function with valid constrained return — cleared isFunctional, ensures passes |
There was a problem hiding this comment.
Why clear isFunctional instead of reporting this case as not supported?
There was a problem hiding this comment.
Without clearing isFunctional, the translator drops the postcondition with a warning but still translates the function — the constraint is not checked at all (we verified contradictory asserts both pass). Clearing it converts to a procedure with ensures, which Core verifies correctly.
Alternative: reject constrained return types on functions entirely. Would you prefer that?
| # Constrained Type Elimination | ||
|
|
||
| A Laurel-to-Laurel pass that eliminates constrained types by: | ||
| 1. Adding `requires` for constrained-typed inputs (Core handles caller asserts and body assumes) |
There was a problem hiding this comment.
I think using requires clauses for constrained types has this downside:
- Unnecessary assertions for calls where the type of the provided value was already constrained
I think using ensures clauses for constrained types has these downsides:
- Transparent procedures and functions (so procedures and functions that did not already have an ensures clause) should not have ensures clauses. Adding an ensures clause leads to duplication of information since everything about the returned value is already visible from the transparent body.
- I think this does not extend to polymorphic procedures
My suggestion would be:
- Replace these requires clauses by:
- Detect casts from base to constrained types and add assertions there.
- Add assumptions at the start of procedures that have constrained parameters
- Replace these ensures clauses by:
- for calls to opaque procedures/functions, assume the constraint of any returned values.
There was a problem hiding this comment.
Agreed the redundancy is real. The current design trades precision for simplicity — the pass only looks at the callee's signature, never at call sites or caller context, keeping it a straightforward Laurel-to-Laurel transformation.
Your cast-based alternative would produce smaller Core programs and reduce SMT work, but needs cast detection, opaque/transparent call distinction, and call-site walking. OK to keep the simpler approach for this PR and refine in a follow-up, or is the redundancy a blocker?
A Laurel-to-Laurel elimination pass (ConstrainedTypeElim.lean) that: - Adds requires for constrained-typed inputs - Adds ensures for constrained-typed outputs - Clears isFunctional when adding ensures (function postconditions not yet supported) - Inserts assert for local variable init and reassignment - Uses witness as default initializer for uninitialized constrained variables - Validates witnesses via synthetic procedures - Injects constraints into quantifier bodies (forall → implies, exists → and) - Resolves all constrained type references to base types - Handles capture avoidance in identifier substitution Core's call elimination handles caller-side argument asserts and return value assumes automatically via requires/ensures. Grammar: constrained type syntax Parser: parseConstrainedType + topLevelConstrainedType Test: T09_ConstrainedTypes — 25 test procedures
fabiomadge
force-pushed
the
fabiomadge/constrained-types
branch
from
afd9ee8 to
56da20a
Compare
2 participants
Constrained Types for Laurel
Adds constrained types to Laurel via a Laurel-to-Laurel elimination pass that inserts verification checks at type boundaries.
Syntax
How it works
The pass (
ConstrainedTypeElim.lean) eliminates constrained types by:requiresfor constrained-typed inputs — Core handles caller asserts and body assumes via call eliminationensuresfor constrained-typed outputs — Core handles body checks and caller assumesassertafter local variable init and reassignment of constrained-typed variablesforall(n: nat) => bodybecomesforall(n: int) => n >= 0 ==> body;existsuses&&The Core translator sees only base types and regular requires/ensures/assert — no translator changes needed beyond pipeline wiring.
Functions
Functions (
isFunctionalprocedures) with constrained return types haveisFunctionalcleared since the Laurel translator does not yet support function postconditions. A TODO marks this for restoration once that support lands.Changes
ConstrainedTypeElim.lean— the elimination passLaurelGrammar.st— constrained type syntaxConcreteToAbstractTreeTranslator.lean— parser forconstrainedkeywordLaurelToCoreTranslator.lean— pipeline wiring (import + pass + resolve)T09_ConstrainedTypes.lean— 24 test procedures covering inputs, outputs, assignments, arguments, nested types, functions, witnesses, quantifiers, capture avoidanceKnown limitations
resolveBaseType,getAllConstraints, andsubstIdarepartial— cyclic constrained type definitions loop forever; capture avoidance prevents a termination proof forsubstIdBy submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.